E, X1, X2:Type, pred?:(E(?E)), info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), r1, r2, x:E.
SWellFounded(((first(y))) c (x = pred(y)))  r2 before r1  eventlist(pred?;x)  r2 < r1 

latex

Definitions

P  Q, x:A. B(x), pred(e), t  T, first(e), b, A, A c B, x,y. t(x;y), Unit, IdLnk, Id, SWellFounded(R(x;y)), eventlist(pred?;e), x before y  l, e < e', , {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), b, , P & Q, P  Q, SQType(T), P  Q, False, R1 => R2, x f y, pred!(e;e'), x.A(x), s = t, sender(e), rcv?(e), R^+

Lemmas

rel plus wf, rel-star-rel-plus, rcv? wf, sender wf, rel plus monotone, pred! wf, member eventlist, member singleton, l before append iff, singleton before, bool cases, eqtt to assert, bool sq, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, cless wf, l before wf, eventlist wf, strongwellfounded wf, Id wf, IdLnk wf, unit wf, strongwf-implies, not wf, assert wf, first wf, pred wf